…ertion (#97)

The false assertion corrected in #95 was **not an isolated slip**.
Auditing whether the conformance corpus actually *runs* — the gate only
ever checked that it *parsed* — turned up a second mathematically false
claim of exactly the same kind, plus one genuine unimplemented feature.

## The second false assertion

`conformance/valid/v16_close_mirror_reverse.tangle`:

```tangle
assert reverse(braid[s1, s2]) == braid[s2, s1]
```

`reverse` reverses the word **and** negates every exponent — it yields
the *inverse* braid, so `reverse(s1 s2) = s2⁻¹ s1⁻¹`.

Disproved by invariant: `writhe(reverse(braid[s1,s2])) = -2` while
`writhe(braid[s2,s1]) = +2`, and writhe is invariant under the braid
relations, so they cannot be the same element.

## Two authors, same mistake → a documentation failure

`examples/trefoil.tangle` and this file made the *identical* wrong
assumption. That is not carelessness. `FORMAL-SEMANTICS.md` described
the operation as:

```
|  reverse(e)     -- reverse word
```

which reads as order-only. Now stated as an identity:

```
reverse(g₁ g₂ … gₙ)  =  gₙ⁻¹ … g₂⁻¹ g₁⁻¹        i.e.  reverse(w) = w⁻¹
```

with the contrast against `mirror` (which negates **in place**) spelled
out, and the writhe argument recorded so the next reader can check it
rather than trust it.

## The systemic fix

`scripts/check-corpus.sh` now **evaluates** `conformance/valid`, not
just parses it. Parsing was never enough — a program can parse perfectly
and assert something false. Both bad assertions survived precisely
because nothing ran them.

**Verified in both directions:** reintroducing the exact false assertion
makes the gate fail (`exit 1`, *"parses but does not evaluate"*);
restoring it returns `exit 0`.

## The genuine gap

`v09_twist.tangle` uses `(~a)` to twist a named strand inside a weave.
`spec/grammar.ebnf` says *"In weave context: (~a) twists named strand
a"*, but `infer_expr` rejects any strand name used as an expression —
specified and unimplemented. Recorded in the new
`CONFORMANCE_KNOWN_UNRUNNABLE` list rather than papered over, and raised
as **#96**.

Worth noting *why* it was invisible: until #93 a weave block could not
be bound to anything, so its body was never evaluated. The construct has
literally never run.

## Regression tests

Four pinning `reverse`, chosen so they cannot pass vacuously:

| Test | Why it can't be faked |
|---|---|
| reverse is **not** order-reversal | asserts inequality with the wrong
answer |
| `reverse(reverse(w)) = w` | only holds if it genuinely inverts |
| reverse negates writhe | the invariant that disproved both false
claims |
| `mirror` negates *in place* | pins the contrast that caused the
confusion |

Suites 112 → 116, all green; TG-3 still 1008/0.

🤖 Generated with [Claude Code](https://claude.com/claude-code)

Co-authored-by: Claude Opus 5 <noreply@anthropic.com>

) (#101)

`conformance/valid/v09_twist.tangle` parsed but failed to typecheck:

```tangle
def twisted =
  weave strands a:Q into
    (~a)
  yield strands a:Q
```
```
Strand name 'a' cannot be used as a standalone expression
```

## The spec licenses it explicitly

`FORMAL-SEMANTICS.md` §3.10:

```
Σ(a) = (i, T)
───────────────────────────────────  [T-Twist-Strand]
Γ; Σ ⊢ (~a) : Tangle[[T], [T]]
```

and `spec/grammar.ebnf`: *"In weave context: `(~a)` twists named strand
a."*

The `Twist` case inferred its operand as an ordinary expression, and the
`Var` rule rejects strand names outright — so the strand-name guard
fired before the twist rule could apply. `[T-Twist-Strand]` is now tried
**first**, leaving `[T-Twist-Word]`/`[T-Twist-Tangle]` to the standalone
forms.

## One of a matched pair was missing

The spec presents this rule immediately alongside `[T-Self-Cross]`:

```
Σ(a) = (i, T)                          Σ(a) = (i, T)
─────────────────────────────────      ─────────────────────────────────
Γ; Σ ⊢ (~a) : Tangle[[T], [T]]         Γ; Σ ⊢ (a > a) : Tangle[[T], [T]]
```

`[T-Self-Cross]` was already implemented; its twin was not. **A test now
pins that the two agree**, so they can't drift apart again.

## Evaluation

Mirrors `Crossing`: structural, yielding the empty word. Weave bodies
only became evaluable in #93, so this construct had **never run**.

That's also defensible mathematically — a single-strand twist is
invisible to the braid *word*: it's a framing change (Reidemeister I)
that the braid group doesn't see.

Detecting it as "a `Var` the environment doesn't bind" is safe because
typechecking runs first and admits `Twist (Var a)` only when `a` is a
strand.

## Result

conformance **16/19 → 17/19 evaluating** (18/19 parse). The corpus
ratchet demanded the manifest update — exactly what it's for.
**`v11_add_block` (#94, the Harvard sub-language) is now the only
remaining gap.**

Tests: the rule itself; agreement with `[T-Self-Cross]`; a regression
guard that standalone twist on a `Word` is unchanged; and that a
nonsense twist still fails.

All suites green; corpus and RSR gates pass.

🤖 Generated with [Claude Code](https://claude.com/claude-code)

Co-authored-by: Claude Opus 5 <noreply@anthropic.com>